COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	exampl[w85,jmc]		Examples for formalization
C00006 ENDMK
C⊗;
exampl[w85,jmc]		Examples for formalization

1. I discover at the Academic Senate that the coat hanging over
the chair isn't mine and conclude that someone took mine.
Returning to my office I find mine.  Then I find a note in
the office saying that I have apparently taken V.M.'s coat.
I conclude that I did and that I didn't notice that the coat
wasn't mine until the end of the Senate meeting.

2. Dogs and trash cans.

3. Little Nell will die if Dudley does nothing about her being
tied to the railroad track.  McDermott points out a problem.
Dudley predicts that Little Nell will die which is bad.  He
therefore decides to save her.  Now he predicts she will live
and therefore decides to do nothing.  --- or something like
that.

Perhaps the troubles with Little Nell have to do with ignoring
the difference between plan time and action time.  The solution
goes like this.  Dudley's plan is to do nothing.  If he carries
out his plan, Little Nell will die which is bad.  Now Dudley
plans to save Little Nell, i.e. he has performed an action of
planning that changes is plan situation.  Now if he carries out
his plan, Little Nell will be saved which is good.  He is now
committed to carry out the plan.

4. Eight queens.  The problem is posed as wanting 8 queens on the
board, no two attacking each other.  The fact that there must be
exactly one queen on each rank and file must be derived from this,
i.e. assuming it is partly solving the problem for the computer.
The problem solver should do the work of eliminating the symmetries.

Suppose we use a general program that successively puts queens
on the board and backtracks.  We may choose to exhaust any set
that may contain one and only one queen.  More genrally, we
may choose any set at any time, but then we must exhaust the
possibilities of how many queens are in that set.

5. Building a traffic light.

6. The light normally stays on until the watchman normally turns it off.